;;; -*- Mode: Lisp; Package: STELLA; Syntax: COMMON-LISP; Base: 10 -*-

(CL:IN-PACKAGE "STELLA")

(IN-MODULE "/PL-KERNEL-KB/PL-FOUNDATION/PL-SYSTEM")

(IN-DIALECT :KIF)

(set-feature iterative-deepening)

;------------------------------------------------------------------------------
; C Basic Definitions
;------------------------------------------------------------------------------

(ASSERT (Being Being_1))
(ASSERT (Being Being_0))

(DEFRELATION  c   ((?x Being) (?y Being))) (ASSERT (closed c))
(DEFRELATION  j   ((?x Being) (?y Being))
:<=> (
	AND (c ?x ?y) (NOT (c ?x Being_0))
)) (ASSERT (closed j))

;------------------------------------------------------------------------------
; C Axioms
;------------------------------------------------------------------------------

; AC1
(ASSERT (
	FORALL ((?x Being) (?y Being)) ( 
		<=>
			(c ?x ?y)
			(FORALL ((?z Being)) (
				=> (c ?z ?x) (c ?z ?y)
			))
	)
))

; AC2
(ASSERT (
	FORALL ((?x Being)) ( 
		AND
			(c ?x Being_1)
			(c Being_0 ?x)
	)
))
; AC2
(ASSERT (
	NOT (c Being_1 Being_0)
))

;------------------------------------------------------------------------------
; C Aristotle Definitions
;------------------------------------------------------------------------------

(DEFRELATION  i   ((?x Being) (?y Being))
:<=> (
	EXISTS ((?z Being)) (
		AND
			(j ?z ?x)
			(j ?z ?y)
	)
)) (ASSERT (closed i))

(DEFRELATION  a   ((?x Being) (?y Being))
:<=> (
	FORALL ((?z Being)) (
		=>
			(j ?z ?x)
			(i ?z ?y)
	)
)) (ASSERT (closed a))

(DEFRELATION  e   ((?x Being) (?y Being))
:<=> (
	FORALL ((?z Being)) (
		=>
			(j ?z ?x)
			(NOT (j ?z ?y))
	)		
)) (ASSERT (closed e))

(DEFRELATION  o   ((?x Being) (?y Being))
:<=> (
	EXISTS ((?z Being)) (
		AND
			(j ?z ?x)
			(e ?z ?y)
	)		
)) (ASSERT (closed o))

;------------------------------------------------------------------------------
; C Additional Definitions
;------------------------------------------------------------------------------

(DEFRELATION  eq  ((?x Being) (?y Being))
:<=> (
	AND (a ?x ?y) (a ?y ?x)
)) (ASSERT (closed eq))

(DEFFUNCTION  ng  ((?x Being)):->(?b Being)) (ASSERT (total ng))
(ASSERT (
	FORALL ((?x Being) (?y Being)) (
		<=>
			(j ?x (ng ?y))
			(AND (j ?x Being_1)(e ?x ?y))
	)
))

;------------------------------------------------------------------------------
; L Basic Definitions
;------------------------------------------------------------------------------

(ASSERT (Being Being_U))
(ASSERT (
	FORALL ((?x Being)) (
		<=>
			(j ?x Being_U)
			(AND 
					(j ?x ?x) 
					(FORALL ((?z Being)) (
							=> (j ?z ?x) (j ?x ?z)
					))
			)
	)
))

(DEFRELATION  eps   ((?x Being) (?y Being))
:<=> (
	AND (j ?x Being_U) (j ?x ?y)
)) (ASSERT (closed eps))

(ASSERT (Being Being_V))
(ASSERT (
	FORALL ((?x Being)) (
		<=>
			(eps ?x Being_V)
			(eps ?x ?x)
	)
))

(ASSERT (Being Being_P))
(ASSERT (
	FORALL ((?x Being)) (
		<=>
			(j ?x Being_P)
			(AND (j ?x Being_1)(NOT (eps ?x Being_V)))
	)
))

(DEFRELATION  c_   ((?x Being) (?y Being))
:<=> (
	FORALL ((?z Being)) (
		=> (eps ?z ?x) (eps ?z ?y)
	)
)) (ASSERT (closed c_))

;------------------------------------------------------------------------------
; L Axioms
;------------------------------------------------------------------------------

; AL1
(ASSERT (
	FORALL ((?x Being) (?y Being)) ( 
		=>
			(FORALL ((?z Being)) (
				=>
					(AND (j ?z Being_U)(j ?z ?x))
					(j ?z ?y)
			))
			(FORALL ((?z Being)) (
				=>
					(j ?z ?x)
					(j ?z ?y)
			))
	)
))

;------------------------------------------------------------------------------
; L Aristotle Definitions
;------------------------------------------------------------------------------

(DEFRELATION  i_   ((?x Being) (?y Being))
:<=> (
	EXISTS ((?z Being)) (
		AND
			(eps ?z ?x)
			(eps ?z ?y)
	)
)) (ASSERT (closed i_))

(DEFRELATION  a_   ((?x Being) (?y Being))
:<=> (
	FORALL ((?z Being)) (
		=>
			(eps ?z ?x)
			(i_ ?z ?y)
	)
)) (ASSERT (closed a_))

(DEFRELATION  e_   ((?x Being) (?y Being))
:<=> (
	FORALL ((?z Being)) (
		=>
			(eps ?z ?x)
			(NOT (eps ?z ?y))
	)		
)) (ASSERT (closed e_))

(DEFRELATION  o_   ((?x Being) (?y Being))
:<=> (
	EXISTS ((?z Being)) (
		AND
			(eps ?z ?x)
			(e_ ?z ?y)
	)		
)) (ASSERT (closed o_))

;------------------------------------------------------------------------------
; L Additional Definitions
;------------------------------------------------------------------------------

(DEFRELATION  eq_  ((?x Being) (?y Being))
:<=> (
	AND (c_ ?x ?y) (c_ ?y ?x)
)) (ASSERT (closed eq_))

(DEFRELATION  eq__  ((?x Being) (?y Being))
:<=> (
	AND (eps ?x ?y) (eps ?y ?x)
)) (ASSERT (closed eq__))

(DEFFUNCTION  ng_  ((?x Being)):->(?b Being)) (ASSERT (total ng_))
(ASSERT (
	FORALL ((?x Being) (?y Being)) (
		<=>
			(eps ?x (ng_ ?y))
			(AND (eps ?x Being_V)(e_ ?x ?y))
	)
))